functor Ir2Mir (S : IR2MIR_STRUCTS) : IR2MIR =
struct
  open S
  structure M = Mir
  structure F = Frame
  structure Ast = F.Ir

  structure E = Env
  structure B = Build(structure Env = E
                      structure Frame = F) 

  structure T = Temp
  structure Err = ErrorMsg

  val tmpNum : int ref = ref 0
  fun gen_tmp () = 
      let val t = !tmpNum
	  val _ = tmpNum := !tmpNum + 1
      in "_T"^Int.toString(t)
      end
   
  fun transLval' x env senv on = 
      let fun trans (Ast.Ptr(tp, lval, pos)) =
              let val (mirnode, size, types) = transLval' lval env senv on
                  val newtype = case types
                                 of  E.Pointer(subtype) => subtype
                                   | _=> (Err.impossible "Impossible type! Should be Pointer!"; 
                                          raise Err.Error)
		  val nsize = E.calTypeSize newtype senv
              in (M.PTREX(mirnode, size), nsize, newtype)
              end
            | trans (Ast.Inarray(lval, exp, s_array, pos)) =
              let val (mirnode, size, types) = transLval' lval env senv on
                  val (cexp, exp') = transExp exp env senv on
		  val _ = if cexp <> []
			  then raise Fail "bug\n"
			  else ()
                  val newtype = case types
                                 of  E.Array(n, subtype) => subtype
                                   | _ => (Err.impossible "Impossible type! Should be Array!";
                                           raise Err.Error)
		  val subexp' = case types
                                 of  E.Array(n, subtype) => (M.ARRAYEX(exp', n))
                                   | _ => (Err.impossible "Impossible type! Should be Array!";
                                           raise Err.Error)
                  val elemSize = E.calTypeSize newtype senv
              in (M.BINOP(M.PLUS, mirnode, (M.BINOP(M.MUL, subexp', M.CONST(elemSize)))), elemSize, newtype)
              end
            | trans (Ast.Instruct(lval, id, pos)) = 
              let val (mirnode, size, types) = transLval' lval env senv on
                  val (offset, newtype) = case types
                                           of  E.Struct(s) => Option.valOf (E.lookupF s id senv)
                                            | _ => (Err.impossible "Impossible type! Should be Struct";
                                                    raise Err.Error)
		  val nsize = E.calTypeSize newtype senv
               in (M.BINOP(M.PLUS, mirnode, M.CONST(offset)), nsize, newtype)
              end
            | trans (Ast.Var(id, pos)) =
              let val (islocal, offset, types) = Option.valOf(E.lookup id env)
              in  if islocal
                  then (M.BINOP(M.PLUS, M.NAME("_rev_ebp_"), M.CONST(offset)), (E.calTypeSize types senv), types)
                  else (M.NAME(id), (E.calTypeSize types senv), types)
              end
	    | trans _ = raise Fail "bug\n"
      in  trans x
      end
  
  and transLval lval env senv on = 
      let val (p1, p2, p3) = transLval' lval env senv on 
      in (p1, p2)
      end 

  and transExp e env senv on = 
      let fun trans (Ast.Expvoid) = ([], M.DUMMY)
            | trans (Ast.IntNum(i)) = ([], M.CONST(i))
            | trans (Ast.True) = ([], M.CONST(1))
            | trans (Ast.False) = ([], M.CONST(0))
            | trans (Ast.Null) = ([], M.CONST(0))
            | trans (Ast.Lval(lval)) = 
              let val (mirnode, size) = transLval lval env senv on
              in ([], M.MEM(mirnode, size))
              end
	    | trans (t as Ast.BinopExp(e1, bop, e2, pos)) = 
	      (fn (Ast.Plus) => let val (dm1, e1') = transExp e1 env senv on
				    val (dm2, e2') = transExp e2 env senv on
				in ([], M.BINOP(M.PLUS, e1', e2'))
				end
		| (Ast.Minus) => let val (dm1, e1') = transExp e1 env senv on
				     val (dm2, e2') = transExp e2 env senv on
				 in ([], M.BINOP(M.MINUS, e1', e2'))
				 end
		| (Ast.Times) => let val (dm1, e1') = transExp e1 env senv on
				     val (dm2, e2') = transExp e2 env senv on
				 in ([], M.BINOP(M.MUL, e1', e2'))
				 end
		| (Ast.Divide) => let val (dm1, e1') = transExp e1 env senv on
				      val (dm2, e2') = transExp e2 env senv on
				  in ([], M.BINOP(M.DIV, e1', e2'))
				  end
		| (Ast.Modus) => let val (dm1, e1') = transExp e1 env senv on
				     val (dm2, e2') = transExp e2 env senv on
				 in ([], M.BINOP(M.MOD, e1', e2'))
				 end
		| (Ast.Band) => let val lb1 = T.newLabel()
				    val lb2 = T.newLabel()
				    val lb3 = T.newLabel()
				    val tmpP = gen_tmp()
				    val conds = transCExp t env senv lb1 lb2 on
				    val conds' = conds@[M.Label(lb1, 0), M.MOV(M.NAME(tmpP), M.CONST(1))]@
						 [M.JMP(lb3),M.Label(lb2, 0), M.MOV(M.NAME(tmpP), M.CONST(0))]@
						 [M.JMP(lb3),M.Label(lb3, 0)]
				in ([], M.TEMP(tmpP, conds'))
				end
		| (Ast.Bor) => let val lb1 = T.newLabel()
				   val lb2 = T.newLabel()
				   val lb3 = T.newLabel()
				   val tmpP = gen_tmp()
				   val conds = transCExp t env senv lb1 lb2 on
				   val conds' = conds@[M.Label(lb1, 0), M.MOV(M.NAME(tmpP), M.CONST(1))]@
						[M.JMP(lb3),M.Label(lb2, 0), M.MOV(M.NAME(tmpP), M.CONST(0))]@
						[M.JMP(lb3),M.Label(lb3, 0)]
			       in ([], M.TEMP(tmpP, conds'))
			       end
		| (Ast.Equ) => let val lb1 = T.newLabel()
				   val lb2 = T.newLabel()
				   val lb3 = T.newLabel()
				   val tmpP = gen_tmp()
				   val conds = transCExp t env senv lb1 lb2 on
				   val conds' = conds@[M.Label(lb1, 0), M.MOV(M.NAME(tmpP), M.CONST(1))]@
						[M.JMP(lb3),M.Label(lb2, 0), M.MOV(M.NAME(tmpP), M.CONST(0))]@
						[M.JMP(lb3),M.Label(lb3, 0)]
			       in ([], M.TEMP(tmpP, conds'))
			       end
		| (Ast.NEqu) => let val lb1 = T.newLabel()
				    val lb2 = T.newLabel()
				    val lb3 = T.newLabel()
				    val tmpP = gen_tmp()
				    val conds = transCExp t env senv lb1 lb2 on
				    val conds' = conds@[M.Label(lb1, 0), M.MOV(M.NAME(tmpP), M.CONST(1))]@
						 [M.JMP(lb3),M.Label(lb2, 0), M.MOV(M.NAME(tmpP), M.CONST(0))]@
						 [M.JMP(lb3),M.Label(lb3, 0)]
				in ([], M.TEMP(tmpP, conds'))
				end
		| (Ast.GT) => let val lb1 = T.newLabel()
				    val lb2 = T.newLabel()
				    val lb3 = T.newLabel()
				    val tmpP = gen_tmp()
				    val conds = transCExp t env senv lb1 lb2 on
				    val conds' = conds@[M.Label(lb1, 0), M.MOV(M.NAME(tmpP), M.CONST(1))]@
						 [M.JMP(lb3),M.Label(lb2, 0), M.MOV(M.NAME(tmpP), M.CONST(0))]@
						 [M.JMP(lb3),M.Label(lb3, 0)]
				in ([], M.TEMP(tmpP, conds'))
				end
		| (Ast.GE) => let val lb1 = T.newLabel()
				  val lb2 = T.newLabel()
				  val lb3 = T.newLabel()
				  val tmpP = gen_tmp()
				  val conds = transCExp t env senv lb1 lb2 on
				  val conds' = conds@[M.Label(lb1, 0), M.MOV(M.NAME(tmpP), M.CONST(1))]@
					       [M.JMP(lb3),M.Label(lb2, 0), M.MOV(M.NAME(tmpP), M.CONST(0))]@
					       [M.JMP(lb3),M.Label(lb3, 0)]
			      in ([], M.TEMP(tmpP, conds'))
			      end
		| (Ast.LT) => let val lb1 = T.newLabel()
				  val lb2 = T.newLabel()
				  val lb3 = T.newLabel()
				  val tmpP = gen_tmp()
				  val conds = transCExp t env senv lb1 lb2 on
				  val conds' = conds@[M.Label(lb1, 0), M.MOV(M.NAME(tmpP), M.CONST(1))]@
					       [M.JMP(lb3),M.Label(lb2, 0), M.MOV(M.NAME(tmpP), M.CONST(0))]@
					       [M.JMP(lb3),M.Label(lb3, 0)]
			      in ([], M.TEMP(tmpP, conds'))
			      end
		| (Ast.LE) => let val lb1 = T.newLabel()
				  val lb2 = T.newLabel()
				  val lb3 = T.newLabel()
				  val tmpP = gen_tmp()
				  val conds = transCExp t env senv lb1 lb2 on
				  val conds' = conds@[M.Label(lb1, 0), M.MOV(M.NAME(tmpP), M.CONST(1))]@
					       [M.JMP(lb3),M.Label(lb2, 0), M.MOV(M.NAME(tmpP), M.CONST(0))]@
					       [M.JMP(lb3),M.Label(lb3, 0)]
			      in ([], M.TEMP(tmpP, conds'))
			      end) bop
	    | trans (Ast.Not(e1, pos)) = 
	      let val lb1 = T.newLabel()
		  val lb2 = T.newLabel()
		  val lb3 = T.newLabel()
		  val tmpP = gen_tmp()
		  val conds = transCExp (Ast.Not(e1, pos)) env senv lb1 lb2 on
		  val conds' = conds@[M.Label(lb1, 0), M.MOV(M.NAME(tmpP), M.CONST(1))]@
			       [M.JMP(lb3),M.Label(lb2, 0), M.MOV(M.NAME(tmpP), M.CONST(0))]@
			       [M.JMP(lb3),M.Label(lb3, 0)]
	      in ([], M.TEMP(tmpP, conds'))
	      end
            | trans (Ast.Imply(e1, e2, pos)) = ([], M.DUMMY) 
            | trans (Ast.Forall(id, mytype, exp, pos)) = ([], M.DUMMY)
            | trans (Ast.Exists(id, mytype, exp, pos)) = ([], M.DUMMY) 
            | trans _ = ([], M.DUMMY)
      in trans e
      end  
  and transCExp ce env senv tbrch fbrch on = 
      let fun trans (Ast.BinopExp(e1, Ast.Equ, e2, pos)) = 
	      let val (dm1, e1') = transExp e1 env senv on
		  val (dm2, e2') = transExp e2 env senv on
	      in [M.CJMP(M.EQ, e1', e2', tbrch, fbrch)]
	      end
	    | trans (Ast.BinopExp(e1, Ast.NEqu, e2, pos)) = 
	      let val (dm1, e1') = transExp e1 env senv on
		  val (dm2, e2') = transExp e2 env senv on
	      in [M.CJMP(M.NE, e1', e2', tbrch, fbrch)]
	      end
	    | trans (Ast.BinopExp(e1, Ast.GT, e2, pos)) = 
	      let val (dm1, e1') = transExp e1 env senv on
		  val (dm2, e2') = transExp e2 env senv on
	      in [M.CJMP(M.GT, e1', e2', tbrch, fbrch)]
	      end
	    | trans (Ast.BinopExp(e1, Ast.GE, e2, pos)) = 
	      let val (dm1, e1') = transExp e1 env senv on
		  val (dm2, e2') = transExp e2 env senv on
	      in [M.CJMP(M.GE, e1', e2', tbrch, fbrch)]
	      end
	    | trans (Ast.BinopExp(e1, Ast.LT, e2, pos)) = 
	      let val (dm1, e1') = transExp e1 env senv on
		  val (dm2, e2') = transExp e2 env senv on
	      in [M.CJMP(M.LT, e1', e2', tbrch, fbrch)]
	      end
	    | trans (Ast.BinopExp(e1, Ast.LE, e2, pos)) = 
	      let val (dm1, e1') = transExp e1 env senv on
		  val (dm2, e2') = transExp e2 env senv on
	      in [M.CJMP(M.LE, e1', e2', tbrch, fbrch)]
	      end
	    | trans (Ast.BinopExp(e1, Ast.Band, e2, pos)) = 
	      let val tlb = T.newLabel()
		  val e1' = transCExp e1 env senv tlb fbrch on
		  val e2' = transCExp e2 env senv tbrch fbrch on
	      in e1'@[M.Label(tlb, 0)]@e2'
	      end
	    | trans (Ast.BinopExp(e1, Ast.Bor, e2, pos)) = 
	      let val tlb = T.newLabel()
		  val e1' = transCExp e1 env senv tbrch tlb on
		  val e2' = transCExp e2 env senv tbrch fbrch on
	      in e1'@[M.Label(tlb, 0)]@e2'
	      end
	    | trans (Ast.Not(e1, pos)) = 
	      let val (dummy, tmp_e) = transExp e1 env senv on
	      in [M.CJMP(M.EQ, tmp_e, M.CONST(1), fbrch, tbrch)]
	      end
	    | trans (Ast.True) = [M.JMP(tbrch)]
	    | trans (Ast.False) = [M.JMP(fbrch)]
	    | trans e = 
	      let val (dummy, tmp_e) = transExp e env senv on
	      in [M.CJMP(M.EQ, tmp_e, M.CONST(1), tbrch, fbrch)]
	      end 
      in trans ce
      end
	 
  fun transStm stm env senv frame on =
      let fun trtype E.Simple = Ast.Int
	    | trtype (E.Struct(str)) = Ast.Struct(str)
	    | trtype (E.Array(sz, tp')) = Ast.Array(sz, (trtype tp'))
	    | trtype (E.Pointer(tp')) = Ast.Pointer(trtype tp')

	  fun trans (Ast.Skip) = []
	    | trans (Ast.AsnExp(lval, Ast.Null, ty, pos)) = 
	      let val (movl, dm1, tp) = transLval' lval env senv on
		  val tp' = trtype tp
	      in[M.MOV(movl, M.PCONST(tp'))]
	      end
            | trans (Ast.AsnExp(lval, exp, ty, pos)) = 
              let val (movl, dm1) = transLval lval env senv on
                  val (prec, movr) = transExp exp env senv on
              in prec@[M.MOV(movl, movr)]
              end 
            | trans (Ast.AsnAlloc(lval, mytype, bty, pos)) = 
              let val (movl, dm1, tp1) = transLval' lval env senv on
                  val tp = (fn E.Pointer(t) => t
                             | _ => raise Fail "bug\n") tp1
		  val tp' = M.PCONST(trtype tp)
                  val size = E.calTypeSize (B.cvtType(mytype)) senv
		  val pas1 = M.CONST(size)
              in  [M.MOV(movl, M.CALL("alloc", [pas1, tp']))]
              end 
            | trans (Ast.AsnCall(lval, fid, explist, ty, pos)) =
              let val (movl, dm1) = transLval lval env senv on
                  val res = transStm (Ast.Call(fid, explist, pos)) env senv frame on
		  val _ = if res = []
			  then raise Fail "bug\n"
			  else ()
		  val res1 = (fn M.EXP(t) => t
			       | _ => raise Fail "bug\n") (List.hd(List.rev(res)))
		  val res2 = List.rev(List.tl(List.rev(res)))
              in res2@[M.MOV(movl, res1)]
              end
            | trans (Ast.Return(exp, pos)) = 
              let val epilog = F.getEpilog frame
                  val (prec, retvalue) = transExp exp env senv on
              in  prec@[M.MOV(M.NAME("_rev_ret_"), retvalue), (M.JMP(epilog))]
              end
            | trans (Ast.Free (exp, pos)) = 
              let val (prec, pas1) = transExp exp env senv on
	      in prec@[M.EXP(M.CALL("free", [pas1]))]
	      end
            | trans (Ast.If(exp, stm1, stm2, pos)) = 
              let val truetag = T.newLabel()
		  val falsetag = T.newLabel()
                  val endtag = T.newLabel()
		  val mirconds = transCExp exp env senv truetag falsetag on
		  val tbch = M.Label(truetag, 0) :: (transStm stm1 env senv frame on)
		  val fbch = M.Label(falsetag, 0) :: (transStm stm2 env senv frame on)
              in  mirconds@tbch@[M.JMP(endtag)]@fbch@[M.JMP(endtag)]@[M.Label(endtag, 0)]
	      end
            | trans (Ast.While (inv, exp, s, pos)) = 
              let val looptag = ".L"^(T.gen_name pos)
		  val truetag = T.newLabel()
                  val falsetag = T.newLabel()
		  val infno = M.newLbInf inv
		  val loophd = (M.JMP(looptag))::[M.Label(looptag, infno)]
		  val mirconds = transCExp exp env senv truetag falsetag on
		  val tbch = M.Label(truetag, 0):: (transStm s env senv frame on)
              in  loophd@mirconds@tbch@[M.JMP(looptag)]@[M.Label(falsetag, 0)]
              end
            | trans (Ast.Seq(s1, s2, pos)) = 
              let val mirlist1 = transStm s1 env senv frame on
		  val mirlist2 = transStm s2 env senv frame on
	      in mirlist1@mirlist2
	      end
            | trans (Ast.Prop(e, pos)) = [] 
            | trans (Ast.Call (fid, explist, pos)) = 
              let fun transExp' env' senv' on' (exp', (t1, t2)) = 
		      let val (o1, o2) = transExp exp' env' senv' on' 
		      in (t1@o1, o2::t2)
		      end
		  val (prec, pas) = List.foldr (transExp' env senv on) ([],[]) explist
	      in prec@[M.EXP(M.CALL(fid, pas))]
	      end
      in  trans stm
      end

  fun transFun (fid, rettype, arg, var, stm, pre, post) env senv has_proof = 
      let val fnum = T.newNum ()
          val frame = F.newFrame fid fnum rettype
          val env1 = B.buildEnv arg env senv frame F.allocArgs
          val newenv = B.buildEnv var env1 senv frame F.allocLocals
	  val mirlist = transStm stm newenv senv frame has_proof
	  val mirinf : M.mir_fun = mirlist
      in  (mirinf, frame, newenv, senv, pre, post)
      end

  fun transData env' senv = 
      let val env = E.toList env' 
          fun filt (id, (islocal, offset, types)) = 
              let val size = Int.div(((E.calTypeSize types senv) + 1), 4)
              in  (id, size)
              end
          fun select (id, (islocal, offset, types)) =
              if offset = ~1 
              then true
              else false
      in  List.map filt (List.filter select env)
      end
      
   fun transProg ast has_proof = 
       let val liblist =  [("print", (false, ~2, E.Simple)),
                           ("printb", (false, ~2, E.Simple)), 
                           ("printp", (false, ~2, E.Simple)),
                           ("alloc", (false, ~2, E.Simple)), 
                           ("free", (false, ~2, E.Simple))]
           val env = ref (E.fromList liblist) 
           val senv = ref (E.creatse ())
           fun build (Ast.ExdecSkip) = ()
             | build (Ast.ExdecStruct(id, fieldlist, pos)) = 
               senv := B.buildSEnv id fieldlist (!senv)
             | build (Ast.ExdecVar(varlist, pos)) = 
               env := B.buildGEnv varlist (!env)
             | build (Ast.ExdecFunc(id, rettype, arg, var, stm, pre, post, pos)) =
               env := B.buildFEnv (id, rettype) (!env)    
             | build (Ast.ExdecSeq(s1, s2, pos)) = (build s1; build s2)
           fun trans (Ast.ExdecFunc(id, rettype, arg, var, stm, pre, post, pos)) = 
               let val t = transFun (id, rettype, arg, var, stm, pre, post) (!env) (!senv) has_proof
	       in [t]
	       end
             | trans (Ast.ExdecSeq(s1, s2, pos)) = (trans s1)@(trans s2)
             | trans _ = []
           val _ = build ast
	   val data = transData (!env) (!senv)
       in  (trans ast, data) 
       end

  fun emitCode ast (has_proof : bool) =
      let val mirlist = transProg ast has_proof
      in  mirlist
      end
end
